$\forall$$A$, $B$:Type, $P$:($A$$\rightarrow\mathbb{P}$), $d$:($x$:$A$$\rightarrow$Dec($P$($x$))), $f$:(\{$x$:$A$$\mid$ $P$($x$)\} $\rightarrow$$B$). p{-}lift($d$;$f$) $\in$ $A$$\rightarrow$($B$ + Top)